i:Id, T:Type, v:(T), x:Id. @i: x:T initially x = v  Dsys 

latex

Definitions	@i: x:T initially x = v, Dsys, t  T, x:A. B(x)
Lemmas	rationals wf, ma-empty wf, ma-single-init wf, msga wf, id-deq wf, Id wf, eqof wf, ifthenelse wf